The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtRewritingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtRewritingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtRewritingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
↳23 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳24 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

b(b(0, y), x) → y
c(c(c(y))) → c(c(a(a(c(b(0, y)), 0), 0)))
a(y, 0) → b(y, 0)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(z0))) → c2(C(c(a(a(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(a(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
A(z0, 0) → c3(B(z0, 0))
S tuples:

C(c(c(z0))) → c2(C(c(a(a(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(a(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
A(z0, 0) → c3(B(z0, 0))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C, A

Compound Symbols:

c2, c3

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(z0, 0) → c3(B(z0, 0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(z0))) → c2(C(c(a(a(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(a(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
S tuples:

C(c(c(z0))) → c2(C(c(a(a(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(a(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(z0))) → c2(C(c(a(a(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(a(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0)) by

C(c(c(x0))) → c2(C(c(b(a(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(b(a(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2
S tuples:

C(c(c(x0))) → c2(C(c(b(a(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

C(c(c(x0))) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(b(a(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
S tuples:

C(c(c(x0))) → c2(C(c(b(a(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(x0))) → c2(C(c(b(a(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0)) by

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))
S tuples:

C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(x0))) → c2(C(c(a(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0)) by

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
S tuples:

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2, c2

(13) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0)) by C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
S tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2, c2

(15) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0))) by C(c(c(z0))) → c2(C(b(a(c(b(0, z0)), 0), 0)))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
C(c(c(z0))) → c2(C(b(a(c(b(0, z0)), 0), 0)))
S tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
C(c(c(z0))) → c2(C(b(a(c(b(0, z0)), 0), 0)))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2, c2

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(z0))) → c2(C(b(a(c(b(0, z0)), 0), 0))) by

C(c(c(x0))) → c2(C(b(b(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0))
C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
C(c(c(x0))) → c2(C(b(b(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2
S tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
C(c(c(x0))) → c2(C(b(b(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2, c2, c2

(19) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace C(c(c(x0))) → c2(C(c(b(b(c(b(0, x0)), 0), 0))), C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0), A(c(b(0, x0)), 0), C(b(0, x0)), B(0, x0)) by C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
C(c(c(x0))) → c2(C(b(b(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2
S tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
C(c(c(x0))) → c2(C(b(b(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2, c2, c2

(21) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

C(c(c(x0))) → c2(C(b(b(c(b(0, x0)), 0), 0)))
C(c(c(x0))) → c2

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(0, z0), z1) → z0
c(c(c(z0))) → c(c(a(a(c(b(0, z0)), 0), 0)))
a(z0, 0) → b(z0, 0)
Tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
S tuples:

C(c(c(x0))) → c2(C(a(a(c(b(0, x0)), 0), 0)), A(a(c(b(0, x0)), 0), 0))
C(c(c(z0))) → c2(C(c(b(b(c(b(0, z0)), 0), 0))), C(a(a(c(b(0, z0)), 0), 0)), A(b(c(b(0, z0)), 0), 0), A(c(b(0, z0)), 0), C(b(0, z0)), B(0, z0))
K tuples:none
Defined Rule Symbols:

b, c, a

Defined Pair Symbols:

C

Compound Symbols:

c2, c2

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3]
transitions:
00() → 0
b0(0, 0) → 1
c0(0) → 2
a0(0, 0) → 3
01() → 4
b1(0, 4) → 3

(24) BOUNDS(O(1), O(n^1))